ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), m:, A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), m:, A:ecl-trans-tuple(ds; da).
ecl-add-throw(A; m)  ecl-trans-tuple{i:l}(ds; da) 

latex

Definitions	x:A. B(x), ecl-trans-tuple{i:l}(ds; da), t  T, ecl-add-throw(A; m), , spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), if b then t else f fi , P  Q, tt, prop{i:l}, ff, x. t(x), , , Unit, P  Q, P  Q, A, A  B, False, x(s),
Lemmas	bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, s-insert wf, l member wf, decl-state wf, ma-valtype wf, nat wf, ecl-trans-tuple wf, fpf wf, Knd wf, Id wf